課程名稱 |
程式語言:函數程式設計 Programming Languages: Functional Programming |
開課學期 |
112-1 |
授課對象 |
管理學院 資訊管理學研究所 |
授課教師 |
穆信成 |
課號 |
IM5064 |
課程識別碼 |
725 U3920 |
班次 |
|
學分 |
3.0 |
全/半年 |
半年 |
必/選修 |
選修 |
上課時間 |
星期四2,3,4(9:10~12:10) |
上課地點 |
管一101 |
備註 |
總人數上限:70人 外系人數限制:10人 |
|
|
課程簡介影片 |
|
核心能力關聯 |
本課程尚未建立核心能力關連 |
課程大綱
|
為確保您我的權利,請尊重智慧財產權及不得非法影印
|
課程概述 |
大綱、講義等詳見課程網站: https://scmu.github.io/plfp/
=========
本課程為「程式語言(Programming Languages)」系列課程之一,著眼點並不是教特定程式語言,而是以函數語言(functional language)為媒介,討論設計程式解決問題的思考方式、設計程式使用的數學與邏輯基礎、以及程式語言與形式符號在其中扮演的角色。其核心概念包括:
- 程式語言是一種形式語言,作為思考的工具。我們用程式語言表達概念,也用程式語言中的形式規則檢驗程式的正確性。
- 函數程設(functional programming)是一種相當簡化的程式設計模型。因為簡單,有更多易於掌握的性質,可作為討論程式語言的基礎。
- 有一整套程式設計理論奠基於歸納法(induction)之上。資料結構可用歸納法定義,其上的程式可用歸納寫成,關於該程式的性質也可用歸納法證明。與之相對的是餘歸納(coinduction).
- 上述兩種方法都不足以定義出所有程式 -- 為此我們將需要允許遞迴 (general recursion) 的模型. 然而,表達力變強大也意味著我們將失去一些好性質。
- 程式設計與定理證明是密切相關、相輔相成的活動。
- 函數語言這樣的簡單模型允許我們做等式推導,可作為一種程式設計方法 -- 將程式「算」出來。
- 好的型別系統常有「只要型別對,程式就會對」的特性。
- 型別系統與邏輯有密切關係:邏輯陳述相當於型別,具有該型別的程式則是該邏輯陳述的證明。
- 型別系統能幫助我們確立程式的正確性,甚至輔助我們寫程式。
- 更強大的型別系統相當於更具表達力的邏輯。同樣地,邏輯變強大的同時,我們也犧牲掉一些好掌握的性質。 |
課程目標 |
以函數語言為起點,瞭解程式語言在語法、語意、與實務面向的課題。 |
課程要求 |
修過程式設計相關課程,有基礎程式設計能力。 |
預期每週課後學習時數 |
|
Office Hours |
|
指定閱讀 |
上課講義。 |
參考書目 |
Introduction to Functional Programming using Haskell (2nd Edition), by Richard Bird.
Prentice Hall, 1998.
Programming in Haskell, by Graham Hutton.
Cambridge University Press, 2007. |
評量方式 (僅供參考) |
|
|